DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2023.10

E-Unification for Second-Order Abstract Syntax

Authors: Nikolai Kudasov

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract

Higher-order unification (HOU) concerns unification of (extensions of) λ-calculus and can be seen as an instance of equational unification (E-unification) modulo βη-equivalence of λ-terms. We study equational unification of terms in languages with arbitrary variable binding constructions modulo arbitrary second-order equational theories. Abstract syntax with general variable binding and parametrised metavariables allows us to work with arbitrary binders without committing to λ-calculus or use inconvenient and error-prone term encodings, leading to a more flexible framework. In this paper, we introduce E-unification for second-order abstract syntax and describe a unification procedure for such problems, merging ideas from both full HOU and general E-unification. We prove that the procedure is sound and complete.

Cite as

Nikolai Kudasov. E-Unification for Second-Order Abstract Syntax. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kudasov:LIPIcs.FSCD.2023.10,
  author =	{Kudasov, Nikolai},
  title =	{{E-Unification for Second-Order Abstract Syntax}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{10:1--10:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.10},
  URN =		{urn:nbn:de:0030-drops-179944},
  doi =		{10.4230/LIPIcs.FSCD.2023.10},
  annote =	{Keywords: E-unification, higher-order unification, second-order abstract syntax}
}

Search Results

Documents authored by Kudasov, Nikolai

E-Unification for Second-Order Abstract Syntax

Abstract

Cite as

Thanks for your feedback!

Could not send message